P1:(es_realizer{i:l}Prop{i'}).
P1()
 (left, right:es_realizer{i:l}. P1(left)  P1(right)  P1(left  right))
 (loc:Id, T:Type{i}, x:Id, v:T. P1(@loc x initially v:T))
 (loc:Id, T:Type{i}, x:Id, L:Knd List. P1(@loc only events in L change x:T))
 (lnk:IdLnk, tag:Id, L:Knd List. P1(only events in L send on lnk with tag))
 (loc:Id, ds:x:Id fp Type{i}, knd:Knd, T:Type{i}, x:Id, f:(State(ds)Tdecl-type{i:l}(ds; x)).
 (P1(@loc effect knd(v:T)  x := f State(ds) v ))
 (ds:x:Id fp Type{i}, knd:Knd, T:Type{i}, l:IdLnk, dt:x:Id fp Type{i},
 (g:(tg:Id(State(ds)T(decl-type{i:l}(dt; tg) List))) List.
 (P1(sends knd(v:T) on l:tagged(g,State(ds),v):dt))
 (loc:Id, ds:x:Id fp Type{i}, a:Id, T:Type{i}, P:(State(ds)TProp{i}).
 (P1(@loc precondition for a(v:T):P State(ds) v))
 (loc:Id, k:Knd, L:Id List. P1(@loc: k writes only members of L))
 (loc:Id, k:Knd, L:IdLnk List. P1(@loc: k sends only on links in L))
 (loc, x:Id, L:Knd List. P1(@loc: only members of L read x))
 {x1:es_realizer{i:l}. P1(x1)} 

latex

Definitions

x:A. B(x), Prop, P  Q, x(s), {T}, t  T, x. t(x), Realizer, , left  right, @loc x initially v:T, @loc only events in L change x:T, only events in L send on lnk with tag, @loc effect knd(v:T)  x := f State(ds) v , sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc precondition for a(v:T):P State(ds) v, @loc: k writes only members of L, @loc: k sends only on links in L, @loc: only members of L read x, Unit,

Lemmas

unit wf, Id wf, Knd wf, IdLnk wf, fpf wf, decl-state wf, decl-type wf, es realizer wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, Rsframe wf, Rframe wf, Rinit wf, Rplus wf, Rnone wf